COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	CS258		MATHEMATICAL THEORY OF COMPUTATION         WINTER 1975
C00004 ENDMK
C⊗;
CS258		MATHEMATICAL THEORY OF COMPUTATION         WINTER 1975


                     PROOF THAT N-N=0


	Attached is a proof of the theorem on which we got stuck last night,
namely N-N=0.

	Somewhere in the middle is the axiom 1 = SUCC 0, but this is merely
an abbreviation to make the proof clearer and not actually necessary.
The following theorems are proved and used as lemmas:

1. ASSOCIATIVITY ∀M N K.((M+N)+K = M+(N+K)).

2. ZEROPLUS: ∀N.(0+M=M).

3. ONEPLUS: ∀N.(1+N = SUCC N).

4. PLUSONE: ∀N.(N+1 = SUCC N).

	The main proof involves proving and then specializing (M+N)-N = M.
The main point of interest is that the induction is done on
λN.(∀M.((M+N)-N = M)), because in making the induction step we need to
use ∀M.((M+N)-N = M) with SUCC M substituted for M.